E theorem prover

E is a modern, high performance theorem prover for full first-order logic with equality.[1] It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E was developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich.

Contents

System

The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation),[2] several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.[2][3][4]

E is implemented in C and portable to most UNIX dialects and the Cygwin environment. It is available under the GNU GPL.[5]

Competitions

The prover has consistently performed well in the CADE ATP System Competition, winning the CNF/MIX category in 2000 and finishing among the top systems ever since.[6] In 2008 it came in second place.[7] In 2009 it won second place in the FOF (full first order logic) and UEQ (unit equational logic) categories and third place (after two versions of Vampire) in CNF (clausal logic).[8] It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.[9] In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.[10]

Applications

E has been integrated into several other theorem provers. It is, with Vampire and SPASS, at the core of Isabelle's Sledgehammer strategy.[11][12] E also is the reasoning engine in SInE[13] and LEO-II[14] and used as the clausification system for iProver.[15]

Applications of E include reasoning on large ontologies,[16] software verification,[17] and software certification.[18]

References

  1. ^ Schulz, Stephan (2002). "E - A Brainiac Theorem Prover". Journal of AI Communications 15 (2/3): 111–126. 
  2. ^ a b Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E---1.0pre. Retrieved 2009-03-24. 
  3. ^ Schulz, Stephan (2004). "System Description: E 0.81". Proceedings of the 2nd International Joint Conference on Automated Reasoning (Springer) LNAI 3097: 223–228. 
  4. ^ Schulz, Stephan (2001). "Learning Search Control Knowledge for Equational Theorem Proving". Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001) (Springer) LNAI 2174: 320–334. 
  5. ^ Schulz, Stephan (2008). "The E Equational Theorem Prover". http://www.eprover.org. Retrieved 2009-03-24. 
  6. ^ Sutcliffe, Geoff. "The CADE ATP System Competition". http://www.cs.miami.edu/~tptp/CASC/. Retrieved 2009-03-24. 
  7. ^ FOF division of CASC in 2008
  8. ^ Sutcliffe, Geoff (2009). "The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4". AI Communications 22 (1): 59–72. http://iospress.metapress.com/content/f94jp575q0h146v7/. Retrieved 2009-12-16. 
  9. ^ Sutcliffe, Geoff (2010). "The CADE ATP System Competition". University of Miami. http://www.cs.miami.edu/~tptp/CASC/J5/. Retrieved 20 July 2010. 
  10. ^ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. http://www.cs.miami.edu/~tptp/CASC/23/. Retrieved 14 August 2011. 
  11. ^ Paulson, Lawrence C. (2008). "Automation for Interactive Proof: Techniques, Lessons and Prospects". Tools and Techniques for Verification of System Infrastructure - A Festschrift in Honour of Professor Michael J. C. Gordon FRS: 29–30. http://ttvsi.gilith.com/ttvsi.pdf#page=39. Retrieved 2009-12-19. 
  12. ^ Meng, Jia; Lawrence C. Paulson (2004). "Experiments on Supporting Interactive Proof Using Resolution". LNCS (Springer) 3097: 372–384}. http://www.springerlink.com/content/btx6b2rrewvmjc9y/. Retrieved 2009-12-16. 
  13. ^ Sutcliffe, Geoff; et al (2009). The 4th IJCAR ATP System Competition. http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf. Retrieved 2009-12-18. 
  14. ^ Benzmüller, Christoph; Lawrence C. Paulson, Frank Theiss , and Arnaud Fietzke (2008). "LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)". LNCS (4th International Joint Conference on Automated Reasoning, IJCAR 2008 Sydney, Australia: Springer) 5195: 162–170. http://www.ags.uni-sb.de/~chris/papers/C26.pdf. 
  15. ^ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic (system description)". LNCS (Springer) 5195: 292–298. http://www.cs.manchester.ac.uk/~korovink/my_pub/iprover_descr_08.pdf. Retrieved 2009-12-18. 
  16. ^ Ramachandran, Deepak; Pace Reagan and Keith Goolsbery (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology". AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications (AAAI). https://www.aaai.org/Papers/Workshops/2005/WS-05-01/WS05-01-006.pdf. 
  17. ^ Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs". ENTCS (4th International Workshop on First-Order Theorem Proving: Elsevier) 86 (1): 109–119. doi:10.1016/S1571-0661(04)80656-X. http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4DDWKNY-ND&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&_docanchor=&view=c&_rerunOrigin=scholar.google&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=7c3d4c7c9b56361f82b30edf963c5443. Retrieved 2009-12-18. 
  18. ^ Denney, Ewen; Bernd Fischer and Johan Schumann (2006). "An Empirical Evaluation of Automated Theorem Provers in Software Certification". International Journal on Artificial Intelligence Tools 15 (1): 81–107. http://eprints.ecs.soton.ac.uk/12355/. 

External links